(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Bool)
(declare-fun f () Bool)
(declare-fun h () Bool)
(declare-fun g () Bool)
(declare-fun j () Bool)
(declare-fun i () Bool)
(declare-fun ab () Bool)
(declare-fun l () Bool)
(declare-fun k () Bool)
(declare-fun m () Bool)
(declare-fun ac () Bool)
(declare-fun p () Bool)
(declare-fun o () Bool)
(declare-fun n () Bool)
(declare-fun ad () Bool)
(declare-fun s () Bool)
(declare-fun ae () Bool)
(declare-fun af () Bool)
(declare-fun q () Bool)
(declare-fun ag () Bool)
(declare-fun ah () Bool)
(declare-fun u () Bool)
(declare-fun v () Bool)
(declare-fun r () Bool)
(declare-fun x () Real)
(declare-fun y () Bool)
(declare-fun t () Bool)
(declare-fun ai () Bool)
(declare-fun aj () Bool)
(declare-fun ak () Bool)
(declare-fun al () Bool)
(declare-fun am () Bool)
(declare-fun an () Bool)
(declare-fun ao () Bool)
(declare-fun ap () Bool)
(declare-fun aq () Bool)
(declare-fun ar () Bool)
(declare-fun C5_VM14 () Bool)
(declare-fun C2_VM14 () Bool)
(declare-fun PriceProv15 () Real)
(declare-fun ProcProv1 () Real)
(declare-fun ProcProv10 () Real)
(declare-fun StorageProv11 () Real)
(declare-fun w () Real)
(declare-fun z () Real)
(assert (= a 4.0))
(assert (or (= b 1.0) (= b 2.0) (= b 3.0) (= b 4.0)))
(assert (or (= c 1.0) (= c 2.0) (= c 3.0) (= c 4.0)))
(assert (or (= d 1.0) (= d 2.0) (= d 3.0) (= aa 3.0) (= aa 4.0)))
(assert (=> (= x z w 60.0) (= StorageProv11 2.0)))
(assert (<= (+ (ite h 1 0) (ite e 1 0)) 1))
(assert (<= (ite j 1 0) (ite i 1 0)))
(assert (<= (+ (ite k 1 0) (ite m 1 0)) 1))
(assert (<= (+ (ite n 1 0) (ite s 1 0)) 1))
(assert (<= (+ (ite n 1 0) (ite ad 1 0)) 1))
(assert (<= (+ (ite u 1 0) (ite r 1 0)) 1))
(assert (<= (+ (ite o 1 0) (ite ad 1 0)) 1))
(assert (<= (+ (ite af 1 0) (ite q 1 0)) 1))
(assert (<= (+ (ite ah 1 0) (ite r 1 0)) 0))
(assert (<= (+ (ite t 1 0) (ite aj 1 0)) 1))
(assert (<= (+ (ite am 1 0) (ite an 1 0)) 1))
(assert (<= (+ (ite e 1 0) (ite g 1 0)) 1 (+ (ite ab 1 0) (ite l 1 0)) 1))
(assert (<= (+ (ite ac 1 0) (ite p 1 0)) 1))
(assert (<= (+ (ite ae 1 0) (ite q 1 0)) 1))
(assert (<= (+ (ite ag 1 0) (ite v 1 0)) 1))
(assert (<= (+ (ite ag 1 0) (ite ah 1 0)) 1))
(assert (<= (+ (ite y 1 0) (ite aj 1 0)) 1))
(assert (<= (+ (ite y 1 0) (ite t 1 0)) 1))
(assert (<= (+ (ite al 1 0) (ite an 1 0)) 1))
(assert (<= (+ (ite al 1 0) (ite am 1 0)) 1))
(assert (<= (ite ao 1 0) (ite aq 1 0)))
(assert (<= (+ (ite C5_VM14 1 0) (ite C2_VM14 1 0)) 1))
(assert (<= (to_real (+ (ite g 2 0) (ite h 4 0) (ite f 4 0) (ite e 4 0))) ProcProv1 ProcProv10))
(assert (<= (ite ai 4 0) (ite t 4 0) (ite y 4 0)))
(assert (<= (+ (* (ite y 1.0 0.0) 4.0)) w))
(assert (<= (+ (* (ite ar 1.0 0.0) (/ 64.0 125.0)) (* (ite aq 1.0 0.0) (/ 64.0 125.0)) (* (ite ap 1.0 0.0) (/ 1.0 2.0)) (* (ite ab 1.0 0.0) (/ 1.0 2.0))) (+ (* (ite s 1.0 0.0)) (* (ite ad 1.0 0.0) 2.0)) (ite o 1.0 0.0)))
(assert (<= (+ (* (ite ak 1.0 0.0)) (* (ite ai 1.0 0.0) (/ 1.0 2.0)) (* (ite t 1.0 0.0))) (* (ite y 1.0 0.0) (/ 1.0 2.0))))
(check-sat)
